Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  iundom2g Structured version   Visualization version   GIF version

Theorem iundom2g 9347
 Description: An upper bound for the cardinality of a disjoint indexed union, with explicit choice principles. 𝐵 depends on 𝑥 and should be thought of as 𝐵(𝑥). (Contributed by Mario Carneiro, 1-Sep-2015.)
Hypotheses
Ref Expression
iunfo.1 𝑇 = 𝑥𝐴 ({𝑥} × 𝐵)
iundomg.2 (𝜑 𝑥𝐴 (𝐶𝑚 𝐵) ∈ AC 𝐴)
iundomg.3 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
Assertion
Ref Expression
iundom2g (𝜑𝑇 ≼ (𝐴 × 𝐶))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐶
Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)   𝑇(𝑥)

Proof of Theorem iundom2g
Dummy variables 𝑓 𝑔 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iundomg.2 . . 3 (𝜑 𝑥𝐴 (𝐶𝑚 𝐵) ∈ AC 𝐴)
2 iundomg.3 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
3 brdomi 7951 . . . . . . . . 9 (𝐵𝐶 → ∃𝑔 𝑔:𝐵1-1𝐶)
43adantl 482 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → ∃𝑔 𝑔:𝐵1-1𝐶)
5 f1f 6088 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐶𝑔:𝐵𝐶)
6 reldom 7946 . . . . . . . . . . . . . . 15 Rel ≼
76brrelex2i 5149 . . . . . . . . . . . . . 14 (𝐵𝐶𝐶 ∈ V)
86brrelexi 5148 . . . . . . . . . . . . . 14 (𝐵𝐶𝐵 ∈ V)
97, 8elmapd 7856 . . . . . . . . . . . . 13 (𝐵𝐶 → (𝑔 ∈ (𝐶𝑚 𝐵) ↔ 𝑔:𝐵𝐶))
109adantl 482 . . . . . . . . . . . 12 ((𝑥𝐴𝐵𝐶) → (𝑔 ∈ (𝐶𝑚 𝐵) ↔ 𝑔:𝐵𝐶))
115, 10syl5ibr 236 . . . . . . . . . . 11 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶𝑔 ∈ (𝐶𝑚 𝐵)))
12 ssiun2 4554 . . . . . . . . . . . . 13 (𝑥𝐴 → (𝐶𝑚 𝐵) ⊆ 𝑥𝐴 (𝐶𝑚 𝐵))
1312adantr 481 . . . . . . . . . . . 12 ((𝑥𝐴𝐵𝐶) → (𝐶𝑚 𝐵) ⊆ 𝑥𝐴 (𝐶𝑚 𝐵))
1413sseld 3594 . . . . . . . . . . 11 ((𝑥𝐴𝐵𝐶) → (𝑔 ∈ (𝐶𝑚 𝐵) → 𝑔 𝑥𝐴 (𝐶𝑚 𝐵)))
1511, 14syld 47 . . . . . . . . . 10 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶𝑔 𝑥𝐴 (𝐶𝑚 𝐵)))
1615ancrd 576 . . . . . . . . 9 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶 → (𝑔 𝑥𝐴 (𝐶𝑚 𝐵) ∧ 𝑔:𝐵1-1𝐶)))
1716eximdv 1844 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → (∃𝑔 𝑔:𝐵1-1𝐶 → ∃𝑔(𝑔 𝑥𝐴 (𝐶𝑚 𝐵) ∧ 𝑔:𝐵1-1𝐶)))
184, 17mpd 15 . . . . . . 7 ((𝑥𝐴𝐵𝐶) → ∃𝑔(𝑔 𝑥𝐴 (𝐶𝑚 𝐵) ∧ 𝑔:𝐵1-1𝐶))
19 df-rex 2915 . . . . . . 7 (∃𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶 ↔ ∃𝑔(𝑔 𝑥𝐴 (𝐶𝑚 𝐵) ∧ 𝑔:𝐵1-1𝐶))
2018, 19sylibr 224 . . . . . 6 ((𝑥𝐴𝐵𝐶) → ∃𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶)
2120ralimiaa 2948 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → ∀𝑥𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶)
222, 21syl 17 . . . 4 (𝜑 → ∀𝑥𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶)
23 nfv 1841 . . . . 5 𝑦𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶
24 nfiu1 4541 . . . . . 6 𝑥 𝑥𝐴 (𝐶𝑚 𝐵)
25 nfcv 2762 . . . . . . 7 𝑥𝑔
26 nfcsb1v 3542 . . . . . . 7 𝑥𝑦 / 𝑥𝐵
27 nfcv 2762 . . . . . . 7 𝑥𝐶
2825, 26, 27nff1 6086 . . . . . 6 𝑥 𝑔:𝑦 / 𝑥𝐵1-1𝐶
2924, 28nfrex 3004 . . . . 5 𝑥𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶
30 csbeq1a 3535 . . . . . . 7 (𝑥 = 𝑦𝐵 = 𝑦 / 𝑥𝐵)
31 f1eq2 6084 . . . . . . 7 (𝐵 = 𝑦 / 𝑥𝐵 → (𝑔:𝐵1-1𝐶𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3230, 31syl 17 . . . . . 6 (𝑥 = 𝑦 → (𝑔:𝐵1-1𝐶𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3332rexbidv 3048 . . . . 5 (𝑥 = 𝑦 → (∃𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶 ↔ ∃𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3423, 29, 33cbvral 3162 . . . 4 (∀𝑥𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝐵1-1𝐶 ↔ ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶)
3522, 34sylib 208 . . 3 (𝜑 → ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶)
36 f1eq1 6083 . . . 4 (𝑔 = (𝑓𝑦) → (𝑔:𝑦 / 𝑥𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
3736acni3 8855 . . 3 (( 𝑥𝐴 (𝐶𝑚 𝐵) ∈ AC 𝐴 ∧ ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶𝑚 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶) → ∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶𝑚 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
381, 35, 37syl2anc 692 . 2 (𝜑 → ∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶𝑚 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
39 nfv 1841 . . . . . 6 𝑦(𝑓𝑥):𝐵1-1𝐶
40 nfcv 2762 . . . . . . 7 𝑥(𝑓𝑦)
4140, 26, 27nff1 6086 . . . . . 6 𝑥(𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶
42 fveq2 6178 . . . . . . . 8 (𝑥 = 𝑦 → (𝑓𝑥) = (𝑓𝑦))
43 f1eq1 6083 . . . . . . . 8 ((𝑓𝑥) = (𝑓𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝐵1-1𝐶))
4442, 43syl 17 . . . . . . 7 (𝑥 = 𝑦 → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝐵1-1𝐶))
45 f1eq2 6084 . . . . . . . 8 (𝐵 = 𝑦 / 𝑥𝐵 → ((𝑓𝑦):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4630, 45syl 17 . . . . . . 7 (𝑥 = 𝑦 → ((𝑓𝑦):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4744, 46bitrd 268 . . . . . 6 (𝑥 = 𝑦 → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4839, 41, 47cbvral 3162 . . . . 5 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ↔ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶)
49 df-ne 2792 . . . . . . . 8 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
50 acnrcl 8850 . . . . . . . . . 10 ( 𝑥𝐴 (𝐶𝑚 𝐵) ∈ AC 𝐴𝐴 ∈ V)
511, 50syl 17 . . . . . . . . 9 (𝜑𝐴 ∈ V)
52 r19.2z 4051 . . . . . . . . . . . 12 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝐵𝐶) → ∃𝑥𝐴 𝐵𝐶)
537rexlimivw 3025 . . . . . . . . . . . 12 (∃𝑥𝐴 𝐵𝐶𝐶 ∈ V)
5452, 53syl 17 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝐵𝐶) → 𝐶 ∈ V)
5554expcom 451 . . . . . . . . . 10 (∀𝑥𝐴 𝐵𝐶 → (𝐴 ≠ ∅ → 𝐶 ∈ V))
562, 55syl 17 . . . . . . . . 9 (𝜑 → (𝐴 ≠ ∅ → 𝐶 ∈ V))
57 xpexg 6945 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 × 𝐶) ∈ V)
5851, 56, 57syl6an 567 . . . . . . . 8 (𝜑 → (𝐴 ≠ ∅ → (𝐴 × 𝐶) ∈ V))
5949, 58syl5bir 233 . . . . . . 7 (𝜑 → (¬ 𝐴 = ∅ → (𝐴 × 𝐶) ∈ V))
60 xpeq1 5118 . . . . . . . 8 (𝐴 = ∅ → (𝐴 × 𝐶) = (∅ × 𝐶))
61 0xp 5189 . . . . . . . . 9 (∅ × 𝐶) = ∅
62 0ex 4781 . . . . . . . . 9 ∅ ∈ V
6361, 62eqeltri 2695 . . . . . . . 8 (∅ × 𝐶) ∈ V
6460, 63syl6eqel 2707 . . . . . . 7 (𝐴 = ∅ → (𝐴 × 𝐶) ∈ V)
6559, 64pm2.61d2 172 . . . . . 6 (𝜑 → (𝐴 × 𝐶) ∈ V)
66 iunfo.1 . . . . . . . . . 10 𝑇 = 𝑥𝐴 ({𝑥} × 𝐵)
6766eleq2i 2691 . . . . . . . . 9 (𝑦𝑇𝑦 𝑥𝐴 ({𝑥} × 𝐵))
68 eliun 4515 . . . . . . . . 9 (𝑦 𝑥𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵))
6967, 68bitri 264 . . . . . . . 8 (𝑦𝑇 ↔ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵))
70 r19.29 3068 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → ∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)))
71 xp1st 7183 . . . . . . . . . . . . . . 15 (𝑦 ∈ ({𝑥} × 𝐵) → (1st𝑦) ∈ {𝑥})
7271ad2antll 764 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) ∈ {𝑥})
73 elsni 4185 . . . . . . . . . . . . . 14 ((1st𝑦) ∈ {𝑥} → (1st𝑦) = 𝑥)
7472, 73syl 17 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) = 𝑥)
75 simpl 473 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥𝐴)
7674, 75eqeltrd 2699 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) ∈ 𝐴)
7774fveq2d 6182 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓‘(1st𝑦)) = (𝑓𝑥))
7877fveq1d 6180 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓𝑥)‘(2nd𝑦)))
79 f1f 6088 . . . . . . . . . . . . . . 15 ((𝑓𝑥):𝐵1-1𝐶 → (𝑓𝑥):𝐵𝐶)
8079ad2antrl 763 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓𝑥):𝐵𝐶)
81 xp2nd 7184 . . . . . . . . . . . . . . 15 (𝑦 ∈ ({𝑥} × 𝐵) → (2nd𝑦) ∈ 𝐵)
8281ad2antll 764 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (2nd𝑦) ∈ 𝐵)
8380, 82ffvelrnd 6346 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓𝑥)‘(2nd𝑦)) ∈ 𝐶)
8478, 83eqeltrd 2699 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st𝑦))‘(2nd𝑦)) ∈ 𝐶)
85 opelxpi 5138 . . . . . . . . . . . 12 (((1st𝑦) ∈ 𝐴 ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) ∈ 𝐶) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8676, 84, 85syl2anc 692 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8786rexlimiva 3024 . . . . . . . . . 10 (∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8870, 87syl 17 . . . . . . . . 9 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8988ex 450 . . . . . . . 8 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶)))
9069, 89syl5bi 232 . . . . . . 7 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑦𝑇 → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶)))
91 fvex 6188 . . . . . . . . . 10 (1st𝑦) ∈ V
92 fvex 6188 . . . . . . . . . 10 ((𝑓‘(1st𝑦))‘(2nd𝑦)) ∈ V
9391, 92opth 4935 . . . . . . . . 9 (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ ((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))))
94 simpr 477 . . . . . . . . . . . . . . 15 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) = (1st𝑧))
9594fveq2d 6182 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (𝑓‘(1st𝑦)) = (𝑓‘(1st𝑧)))
9695fveq1d 6180 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → ((𝑓‘(1st𝑦))‘(2nd𝑧)) = ((𝑓‘(1st𝑧))‘(2nd𝑧)))
9796eqeq2d 2630 . . . . . . . . . . . 12 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))))
98 djussxp 5256 . . . . . . . . . . . . . . . . . 18 𝑥𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V)
9966, 98eqsstri 3627 . . . . . . . . . . . . . . . . 17 𝑇 ⊆ (𝐴 × V)
100 simprl 793 . . . . . . . . . . . . . . . . 17 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑦𝑇)
10199, 100sseldi 3593 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑦 ∈ (𝐴 × V))
102101adantr 481 . . . . . . . . . . . . . . 15 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → 𝑦 ∈ (𝐴 × V))
103 xp1st 7183 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝐴 × V) → (1st𝑦) ∈ 𝐴)
104102, 103syl 17 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) ∈ 𝐴)
105 simpll 789 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → ∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶)
106 nfcv 2762 . . . . . . . . . . . . . . . 16 𝑥(𝑓‘(1st𝑦))
107 nfcsb1v 3542 . . . . . . . . . . . . . . . 16 𝑥(1st𝑦) / 𝑥𝐵
108106, 107, 27nff1 6086 . . . . . . . . . . . . . . 15 𝑥(𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶
109 fveq2 6178 . . . . . . . . . . . . . . . . 17 (𝑥 = (1st𝑦) → (𝑓𝑥) = (𝑓‘(1st𝑦)))
110 f1eq1 6083 . . . . . . . . . . . . . . . . 17 ((𝑓𝑥) = (𝑓‘(1st𝑦)) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):𝐵1-1𝐶))
111109, 110syl 17 . . . . . . . . . . . . . . . 16 (𝑥 = (1st𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):𝐵1-1𝐶))
112 csbeq1a 3535 . . . . . . . . . . . . . . . . 17 (𝑥 = (1st𝑦) → 𝐵 = (1st𝑦) / 𝑥𝐵)
113 f1eq2 6084 . . . . . . . . . . . . . . . . 17 (𝐵 = (1st𝑦) / 𝑥𝐵 → ((𝑓‘(1st𝑦)):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
114112, 113syl 17 . . . . . . . . . . . . . . . 16 (𝑥 = (1st𝑦) → ((𝑓‘(1st𝑦)):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
115111, 114bitrd 268 . . . . . . . . . . . . . . 15 (𝑥 = (1st𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
116108, 115rspc 3298 . . . . . . . . . . . . . 14 ((1st𝑦) ∈ 𝐴 → (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
117104, 105, 116sylc 65 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶)
118107nfel2 2778 . . . . . . . . . . . . . . . . . . . 20 𝑥(2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵
11974eqcomd 2626 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥 = (1st𝑦))
120119, 112syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝐵 = (1st𝑦) / 𝑥𝐵)
12182, 120eleqtrd 2701 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
122121ex 450 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐴 → (((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
123118, 122rexlimi 3020 . . . . . . . . . . . . . . . . . . 19 (∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
12470, 123syl 17 . . . . . . . . . . . . . . . . . 18 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
125124ex 450 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
12669, 125syl5bi 232 . . . . . . . . . . . . . . . 16 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑦𝑇 → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
127126imp 445 . . . . . . . . . . . . . . 15 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑦𝑇) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
128127adantrr 752 . . . . . . . . . . . . . 14 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
129128adantr 481 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
130126ralrimiv 2962 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ∀𝑦𝑇 (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
131 fveq2 6178 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (2nd𝑦) = (2nd𝑧))
132 fveq2 6178 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑧 → (1st𝑦) = (1st𝑧))
133132csbeq1d 3533 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧(1st𝑦) / 𝑥𝐵 = (1st𝑧) / 𝑥𝐵)
134131, 133eleq12d 2693 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵 ↔ (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵))
135134rspccva 3303 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝑇 (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵𝑧𝑇) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
136130, 135sylan 488 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑧𝑇) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
137136adantrl 751 . . . . . . . . . . . . . . 15 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
138137adantr 481 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
13994csbeq1d 3533 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) / 𝑥𝐵 = (1st𝑧) / 𝑥𝐵)
140138, 139eleqtrrd 2702 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑧) ∈ (1st𝑦) / 𝑥𝐵)
141 f1fveq 6504 . . . . . . . . . . . . 13 (((𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶 ∧ ((2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵 ∧ (2nd𝑧) ∈ (1st𝑦) / 𝑥𝐵)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
142117, 129, 140, 141syl12anc 1322 . . . . . . . . . . . 12 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
14397, 142bitr3d 270 . . . . . . . . . . 11 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
144143pm5.32da 672 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))) ↔ ((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧))))
145 simprr 795 . . . . . . . . . . . 12 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑧𝑇)
14699, 145sseldi 3593 . . . . . . . . . . 11 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑧 ∈ (𝐴 × V))
147 xpopth 7192 . . . . . . . . . . 11 ((𝑦 ∈ (𝐴 × V) ∧ 𝑧 ∈ (𝐴 × V)) → (((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧)) ↔ 𝑦 = 𝑧))
148101, 146, 147syl2anc 692 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧)) ↔ 𝑦 = 𝑧))
149144, 148bitrd 268 . . . . . . . . 9 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))) ↔ 𝑦 = 𝑧))
15093, 149syl5bb 272 . . . . . . . 8 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ 𝑦 = 𝑧))
151150ex 450 . . . . . . 7 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ((𝑦𝑇𝑧𝑇) → (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ 𝑦 = 𝑧)))
15290, 151dom2d 7981 . . . . . 6 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ((𝐴 × 𝐶) ∈ V → 𝑇 ≼ (𝐴 × 𝐶)))
15365, 152syl5com 31 . . . . 5 (𝜑 → (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑇 ≼ (𝐴 × 𝐶)))
15448, 153syl5bir 233 . . . 4 (𝜑 → (∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶𝑇 ≼ (𝐴 × 𝐶)))
155154adantld 483 . . 3 (𝜑 → ((𝑓:𝐴 𝑥𝐴 (𝐶𝑚 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶) → 𝑇 ≼ (𝐴 × 𝐶)))
156155exlimdv 1859 . 2 (𝜑 → (∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶𝑚 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶) → 𝑇 ≼ (𝐴 × 𝐶)))
15738, 156mpd 15 1 (𝜑𝑇 ≼ (𝐴 × 𝐶))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1481  ∃wex 1702   ∈ wcel 1988   ≠ wne 2791  ∀wral 2909  ∃wrex 2910  Vcvv 3195  ⦋csb 3526   ⊆ wss 3567  ∅c0 3907  {csn 4168  ⟨cop 4174  ∪ ciun 4511   class class class wbr 4644   × cxp 5102  ⟶wf 5872  –1-1→wf1 5873  ‘cfv 5876  (class class class)co 6635  1st c1st 7151  2nd c2nd 7152   ↑𝑚 cmap 7842   ≼ cdom 7938  AC wacn 8749 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-ral 2914  df-rex 2915  df-reu 2916  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-id 5014  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-1st 7153  df-2nd 7154  df-map 7844  df-dom 7942  df-acn 8753 This theorem is referenced by:  iundomg  9348  iundom  9349
 Copyright terms: Public domain W3C validator