Насчёт учебника советовать не буду, но у меня тоже было желание "посмотреть на строго формализованные доказательства", - и мне в этом очень помог проект
Metamath proof explorer, авторы сперва полностью формулируют финитарные средства и синтаксис на человеческом языке, которые, с точностью до синтаксического сахара, эквивалентны ZFC в формулировке логики предикатов первого порядка c её этой самой "гипотетично дедуктивной моделью", а всё остальное же делается абсолютно формально, на машинном уровне строгости. В принципе - это в точности самый мейнстримовый подход к основаниям математики, который можно назвать "ZFC-центрированым формализмом" что ли (название я придумал, люблю придумвать!).
Существование декартового произведения там тоже есть, но это не очень пример, так как там слишком много средств используется (но если чуть-чуть привыкнуть, то можно читать и такие доказательства, тем более, оно относительно короткое). Но вообще потыкать на
теоремы из списка лично мне было интересно.
Надеюсь, я правильно понял ваш запрос.