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

Theorem iundom2g 10476
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 (𝜑 𝑥𝐴 (𝐶m 𝐵) ∈ 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 (𝜑 𝑥𝐴 (𝐶m 𝐵) ∈ AC 𝐴)
2 iundomg.3 . . . . 5 (𝜑 → ∀𝑥𝐴 𝐵𝐶)
3 brdomi 8898 . . . . . . . . 9 (𝐵𝐶 → ∃𝑔 𝑔:𝐵1-1𝐶)
43adantl 482 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → ∃𝑔 𝑔:𝐵1-1𝐶)
5 f1f 6738 . . . . . . . . . . . 12 (𝑔:𝐵1-1𝐶𝑔:𝐵𝐶)
6 reldom 8889 . . . . . . . . . . . . . . 15 Rel ≼
76brrelex2i 5689 . . . . . . . . . . . . . 14 (𝐵𝐶𝐶 ∈ V)
86brrelex1i 5688 . . . . . . . . . . . . . 14 (𝐵𝐶𝐵 ∈ V)
97, 8elmapd 8779 . . . . . . . . . . . . 13 (𝐵𝐶 → (𝑔 ∈ (𝐶m 𝐵) ↔ 𝑔:𝐵𝐶))
109adantl 482 . . . . . . . . . . . 12 ((𝑥𝐴𝐵𝐶) → (𝑔 ∈ (𝐶m 𝐵) ↔ 𝑔:𝐵𝐶))
115, 10syl5ibr 245 . . . . . . . . . . 11 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶𝑔 ∈ (𝐶m 𝐵)))
12 ssiun2 5007 . . . . . . . . . . . . 13 (𝑥𝐴 → (𝐶m 𝐵) ⊆ 𝑥𝐴 (𝐶m 𝐵))
1312adantr 481 . . . . . . . . . . . 12 ((𝑥𝐴𝐵𝐶) → (𝐶m 𝐵) ⊆ 𝑥𝐴 (𝐶m 𝐵))
1413sseld 3943 . . . . . . . . . . 11 ((𝑥𝐴𝐵𝐶) → (𝑔 ∈ (𝐶m 𝐵) → 𝑔 𝑥𝐴 (𝐶m 𝐵)))
1511, 14syld 47 . . . . . . . . . 10 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶𝑔 𝑥𝐴 (𝐶m 𝐵)))
1615ancrd 552 . . . . . . . . 9 ((𝑥𝐴𝐵𝐶) → (𝑔:𝐵1-1𝐶 → (𝑔 𝑥𝐴 (𝐶m 𝐵) ∧ 𝑔:𝐵1-1𝐶)))
1716eximdv 1920 . . . . . . . 8 ((𝑥𝐴𝐵𝐶) → (∃𝑔 𝑔:𝐵1-1𝐶 → ∃𝑔(𝑔 𝑥𝐴 (𝐶m 𝐵) ∧ 𝑔:𝐵1-1𝐶)))
184, 17mpd 15 . . . . . . 7 ((𝑥𝐴𝐵𝐶) → ∃𝑔(𝑔 𝑥𝐴 (𝐶m 𝐵) ∧ 𝑔:𝐵1-1𝐶))
19 df-rex 3074 . . . . . . 7 (∃𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶 ↔ ∃𝑔(𝑔 𝑥𝐴 (𝐶m 𝐵) ∧ 𝑔:𝐵1-1𝐶))
2018, 19sylibr 233 . . . . . 6 ((𝑥𝐴𝐵𝐶) → ∃𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶)
2120ralimiaa 3085 . . . . 5 (∀𝑥𝐴 𝐵𝐶 → ∀𝑥𝐴𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶)
222, 21syl 17 . . . 4 (𝜑 → ∀𝑥𝐴𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶)
23 nfv 1917 . . . . 5 𝑦𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶
24 nfiu1 4988 . . . . . 6 𝑥 𝑥𝐴 (𝐶m 𝐵)
25 nfcv 2907 . . . . . . 7 𝑥𝑔
26 nfcsb1v 3880 . . . . . . 7 𝑥𝑦 / 𝑥𝐵
27 nfcv 2907 . . . . . . 7 𝑥𝐶
2825, 26, 27nff1 6736 . . . . . 6 𝑥 𝑔:𝑦 / 𝑥𝐵1-1𝐶
2924, 28nfrexw 3296 . . . . 5 𝑥𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶
30 csbeq1a 3869 . . . . . . 7 (𝑥 = 𝑦𝐵 = 𝑦 / 𝑥𝐵)
31 f1eq2 6734 . . . . . . 7 (𝐵 = 𝑦 / 𝑥𝐵 → (𝑔:𝐵1-1𝐶𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3230, 31syl 17 . . . . . 6 (𝑥 = 𝑦 → (𝑔:𝐵1-1𝐶𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3332rexbidv 3175 . . . . 5 (𝑥 = 𝑦 → (∃𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶 ↔ ∃𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶))
3423, 29, 33cbvralw 3289 . . . 4 (∀𝑥𝐴𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝐵1-1𝐶 ↔ ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶)
3522, 34sylib 217 . . 3 (𝜑 → ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶)
36 f1eq1 6733 . . . 4 (𝑔 = (𝑓𝑦) → (𝑔:𝑦 / 𝑥𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
3736acni3 9983 . . 3 (( 𝑥𝐴 (𝐶m 𝐵) ∈ AC 𝐴 ∧ ∀𝑦𝐴𝑔 𝑥𝐴 (𝐶m 𝐵)𝑔:𝑦 / 𝑥𝐵1-1𝐶) → ∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶m 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
381, 35, 37syl2anc 584 . 2 (𝜑 → ∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶m 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
39 nfv 1917 . . . . . 6 𝑦(𝑓𝑥):𝐵1-1𝐶
40 nfcv 2907 . . . . . . 7 𝑥(𝑓𝑦)
4140, 26, 27nff1 6736 . . . . . 6 𝑥(𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶
42 fveq2 6842 . . . . . . . 8 (𝑥 = 𝑦 → (𝑓𝑥) = (𝑓𝑦))
43 f1eq1 6733 . . . . . . . 8 ((𝑓𝑥) = (𝑓𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝐵1-1𝐶))
4442, 43syl 17 . . . . . . 7 (𝑥 = 𝑦 → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝐵1-1𝐶))
45 f1eq2 6734 . . . . . . . 8 (𝐵 = 𝑦 / 𝑥𝐵 → ((𝑓𝑦):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4630, 45syl 17 . . . . . . 7 (𝑥 = 𝑦 → ((𝑓𝑦):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4744, 46bitrd 278 . . . . . 6 (𝑥 = 𝑦 → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶))
4839, 41, 47cbvralw 3289 . . . . 5 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ↔ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶)
49 df-ne 2944 . . . . . . . 8 (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
50 acnrcl 9978 . . . . . . . . . 10 ( 𝑥𝐴 (𝐶m 𝐵) ∈ AC 𝐴𝐴 ∈ V)
511, 50syl 17 . . . . . . . . 9 (𝜑𝐴 ∈ V)
52 r19.2z 4452 . . . . . . . . . . . 12 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝐵𝐶) → ∃𝑥𝐴 𝐵𝐶)
537rexlimivw 3148 . . . . . . . . . . . 12 (∃𝑥𝐴 𝐵𝐶𝐶 ∈ V)
5452, 53syl 17 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴 𝐵𝐶) → 𝐶 ∈ V)
5554expcom 414 . . . . . . . . . 10 (∀𝑥𝐴 𝐵𝐶 → (𝐴 ≠ ∅ → 𝐶 ∈ V))
562, 55syl 17 . . . . . . . . 9 (𝜑 → (𝐴 ≠ ∅ → 𝐶 ∈ V))
57 xpexg 7684 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝐶 ∈ V) → (𝐴 × 𝐶) ∈ V)
5851, 56, 57syl6an 682 . . . . . . . 8 (𝜑 → (𝐴 ≠ ∅ → (𝐴 × 𝐶) ∈ V))
5949, 58biimtrrid 242 . . . . . . 7 (𝜑 → (¬ 𝐴 = ∅ → (𝐴 × 𝐶) ∈ V))
60 xpeq1 5647 . . . . . . . 8 (𝐴 = ∅ → (𝐴 × 𝐶) = (∅ × 𝐶))
61 0xp 5730 . . . . . . . . 9 (∅ × 𝐶) = ∅
62 0ex 5264 . . . . . . . . 9 ∅ ∈ V
6361, 62eqeltri 2834 . . . . . . . 8 (∅ × 𝐶) ∈ V
6460, 63eqeltrdi 2846 . . . . . . 7 (𝐴 = ∅ → (𝐴 × 𝐶) ∈ V)
6559, 64pm2.61d2 181 . . . . . 6 (𝜑 → (𝐴 × 𝐶) ∈ V)
66 iunfo.1 . . . . . . . . . 10 𝑇 = 𝑥𝐴 ({𝑥} × 𝐵)
6766eleq2i 2829 . . . . . . . . 9 (𝑦𝑇𝑦 𝑥𝐴 ({𝑥} × 𝐵))
68 eliun 4958 . . . . . . . . 9 (𝑦 𝑥𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵))
6967, 68bitri 274 . . . . . . . 8 (𝑦𝑇 ↔ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵))
70 r19.29 3117 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → ∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)))
71 xp1st 7953 . . . . . . . . . . . . . . 15 (𝑦 ∈ ({𝑥} × 𝐵) → (1st𝑦) ∈ {𝑥})
7271ad2antll 727 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) ∈ {𝑥})
73 elsni 4603 . . . . . . . . . . . . . 14 ((1st𝑦) ∈ {𝑥} → (1st𝑦) = 𝑥)
7472, 73syl 17 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) = 𝑥)
75 simpl 483 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥𝐴)
7674, 75eqeltrd 2838 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (1st𝑦) ∈ 𝐴)
7774fveq2d 6846 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓‘(1st𝑦)) = (𝑓𝑥))
7877fveq1d 6844 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓𝑥)‘(2nd𝑦)))
79 f1f 6738 . . . . . . . . . . . . . . 15 ((𝑓𝑥):𝐵1-1𝐶 → (𝑓𝑥):𝐵𝐶)
8079ad2antrl 726 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (𝑓𝑥):𝐵𝐶)
81 xp2nd 7954 . . . . . . . . . . . . . . 15 (𝑦 ∈ ({𝑥} × 𝐵) → (2nd𝑦) ∈ 𝐵)
8281ad2antll 727 . . . . . . . . . . . . . 14 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (2nd𝑦) ∈ 𝐵)
8380, 82ffvelcdmd 7036 . . . . . . . . . . . . 13 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓𝑥)‘(2nd𝑦)) ∈ 𝐶)
8478, 83eqeltrd 2838 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ((𝑓‘(1st𝑦))‘(2nd𝑦)) ∈ 𝐶)
8576, 84opelxpd 5671 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8685rexlimiva 3144 . . . . . . . . . 10 (∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8770, 86syl 17 . . . . . . . . 9 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶))
8887ex 413 . . . . . . . 8 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶)))
8969, 88biimtrid 241 . . . . . . 7 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑦𝑇 → ⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ ∈ (𝐴 × 𝐶)))
90 fvex 6855 . . . . . . . . . 10 (1st𝑦) ∈ V
91 fvex 6855 . . . . . . . . . 10 ((𝑓‘(1st𝑦))‘(2nd𝑦)) ∈ V
9290, 91opth 5433 . . . . . . . . 9 (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ ((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))))
93 simpr 485 . . . . . . . . . . . . . . 15 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) = (1st𝑧))
9493fveq2d 6846 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (𝑓‘(1st𝑦)) = (𝑓‘(1st𝑧)))
9594fveq1d 6844 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → ((𝑓‘(1st𝑦))‘(2nd𝑧)) = ((𝑓‘(1st𝑧))‘(2nd𝑧)))
9695eqeq2d 2747 . . . . . . . . . . . 12 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))))
97 djussxp 5801 . . . . . . . . . . . . . . . . . 18 𝑥𝐴 ({𝑥} × 𝐵) ⊆ (𝐴 × V)
9866, 97eqsstri 3978 . . . . . . . . . . . . . . . . 17 𝑇 ⊆ (𝐴 × V)
99 simprl 769 . . . . . . . . . . . . . . . . 17 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑦𝑇)
10098, 99sselid 3942 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑦 ∈ (𝐴 × V))
101100adantr 481 . . . . . . . . . . . . . . 15 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → 𝑦 ∈ (𝐴 × V))
102 xp1st 7953 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝐴 × V) → (1st𝑦) ∈ 𝐴)
103101, 102syl 17 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) ∈ 𝐴)
104 simpll 765 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → ∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶)
105 nfcv 2907 . . . . . . . . . . . . . . . 16 𝑥(𝑓‘(1st𝑦))
106 nfcsb1v 3880 . . . . . . . . . . . . . . . 16 𝑥(1st𝑦) / 𝑥𝐵
107105, 106, 27nff1 6736 . . . . . . . . . . . . . . 15 𝑥(𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶
108 fveq2 6842 . . . . . . . . . . . . . . . . 17 (𝑥 = (1st𝑦) → (𝑓𝑥) = (𝑓‘(1st𝑦)))
109 f1eq1 6733 . . . . . . . . . . . . . . . . 17 ((𝑓𝑥) = (𝑓‘(1st𝑦)) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):𝐵1-1𝐶))
110108, 109syl 17 . . . . . . . . . . . . . . . 16 (𝑥 = (1st𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):𝐵1-1𝐶))
111 csbeq1a 3869 . . . . . . . . . . . . . . . . 17 (𝑥 = (1st𝑦) → 𝐵 = (1st𝑦) / 𝑥𝐵)
112 f1eq2 6734 . . . . . . . . . . . . . . . . 17 (𝐵 = (1st𝑦) / 𝑥𝐵 → ((𝑓‘(1st𝑦)):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
113111, 112syl 17 . . . . . . . . . . . . . . . 16 (𝑥 = (1st𝑦) → ((𝑓‘(1st𝑦)):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
114110, 113bitrd 278 . . . . . . . . . . . . . . 15 (𝑥 = (1st𝑦) → ((𝑓𝑥):𝐵1-1𝐶 ↔ (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
115107, 114rspc 3569 . . . . . . . . . . . . . 14 ((1st𝑦) ∈ 𝐴 → (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶))
116103, 104, 115sylc 65 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶)
117106nfel2 2925 . . . . . . . . . . . . . . . . . . . 20 𝑥(2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵
11874eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝑥 = (1st𝑦))
119118, 111syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → 𝐵 = (1st𝑦) / 𝑥𝐵)
12082, 119eleqtrd 2840 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥𝐴 ∧ ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵))) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
121120ex 413 . . . . . . . . . . . . . . . . . . . 20 (𝑥𝐴 → (((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
122117, 121rexlimi 3242 . . . . . . . . . . . . . . . . . . 19 (∃𝑥𝐴 ((𝑓𝑥):𝐵1-1𝐶𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
12370, 122syl 17 . . . . . . . . . . . . . . . . . 18 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ ∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
124123ex 413 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (∃𝑥𝐴 𝑦 ∈ ({𝑥} × 𝐵) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
12569, 124biimtrid 241 . . . . . . . . . . . . . . . 16 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → (𝑦𝑇 → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵))
126125imp 407 . . . . . . . . . . . . . . 15 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑦𝑇) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
127126adantrr 715 . . . . . . . . . . . . . 14 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
128127adantr 481 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
129125ralrimiv 3142 . . . . . . . . . . . . . . . . 17 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ∀𝑦𝑇 (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵)
130 fveq2 6842 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧 → (2nd𝑦) = (2nd𝑧))
131 fveq2 6842 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑧 → (1st𝑦) = (1st𝑧))
132131csbeq1d 3859 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑧(1st𝑦) / 𝑥𝐵 = (1st𝑧) / 𝑥𝐵)
133130, 132eleq12d 2832 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑧 → ((2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵 ↔ (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵))
134133rspccva 3580 . . . . . . . . . . . . . . . . 17 ((∀𝑦𝑇 (2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵𝑧𝑇) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
135129, 134sylan 580 . . . . . . . . . . . . . . . 16 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑧𝑇) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
136135adantrl 714 . . . . . . . . . . . . . . 15 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
137136adantr 481 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑧) ∈ (1st𝑧) / 𝑥𝐵)
13893csbeq1d 3859 . . . . . . . . . . . . . 14 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (1st𝑦) / 𝑥𝐵 = (1st𝑧) / 𝑥𝐵)
139137, 138eleqtrrd 2841 . . . . . . . . . . . . 13 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (2nd𝑧) ∈ (1st𝑦) / 𝑥𝐵)
140 f1fveq 7209 . . . . . . . . . . . . 13 (((𝑓‘(1st𝑦)):(1st𝑦) / 𝑥𝐵1-1𝐶 ∧ ((2nd𝑦) ∈ (1st𝑦) / 𝑥𝐵 ∧ (2nd𝑧) ∈ (1st𝑦) / 𝑥𝐵)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
141116, 128, 139, 140syl12anc 835 . . . . . . . . . . . 12 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑦))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
14296, 141bitr3d 280 . . . . . . . . . . 11 (((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) ∧ (1st𝑦) = (1st𝑧)) → (((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧)) ↔ (2nd𝑦) = (2nd𝑧)))
143142pm5.32da 579 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))) ↔ ((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧))))
144 simprr 771 . . . . . . . . . . . 12 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑧𝑇)
14598, 144sselid 3942 . . . . . . . . . . 11 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → 𝑧 ∈ (𝐴 × V))
146 xpopth 7962 . . . . . . . . . . 11 ((𝑦 ∈ (𝐴 × V) ∧ 𝑧 ∈ (𝐴 × V)) → (((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧)) ↔ 𝑦 = 𝑧))
147100, 145, 146syl2anc 584 . . . . . . . . . 10 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ (2nd𝑦) = (2nd𝑧)) ↔ 𝑦 = 𝑧))
148143, 147bitrd 278 . . . . . . . . 9 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (((1st𝑦) = (1st𝑧) ∧ ((𝑓‘(1st𝑦))‘(2nd𝑦)) = ((𝑓‘(1st𝑧))‘(2nd𝑧))) ↔ 𝑦 = 𝑧))
14992, 148bitrid 282 . . . . . . . 8 ((∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 ∧ (𝑦𝑇𝑧𝑇)) → (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ 𝑦 = 𝑧))
150149ex 413 . . . . . . 7 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ((𝑦𝑇𝑧𝑇) → (⟨(1st𝑦), ((𝑓‘(1st𝑦))‘(2nd𝑦))⟩ = ⟨(1st𝑧), ((𝑓‘(1st𝑧))‘(2nd𝑧))⟩ ↔ 𝑦 = 𝑧)))
15189, 150dom2d 8933 . . . . . 6 (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶 → ((𝐴 × 𝐶) ∈ V → 𝑇 ≼ (𝐴 × 𝐶)))
15265, 151syl5com 31 . . . . 5 (𝜑 → (∀𝑥𝐴 (𝑓𝑥):𝐵1-1𝐶𝑇 ≼ (𝐴 × 𝐶)))
15348, 152biimtrrid 242 . . . 4 (𝜑 → (∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶𝑇 ≼ (𝐴 × 𝐶)))
154153adantld 491 . . 3 (𝜑 → ((𝑓:𝐴 𝑥𝐴 (𝐶m 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶) → 𝑇 ≼ (𝐴 × 𝐶)))
155154exlimdv 1936 . 2 (𝜑 → (∃𝑓(𝑓:𝐴 𝑥𝐴 (𝐶m 𝐵) ∧ ∀𝑦𝐴 (𝑓𝑦):𝑦 / 𝑥𝐵1-1𝐶) → 𝑇 ≼ (𝐴 × 𝐶)))
15638, 155mpd 15 1 (𝜑𝑇 ≼ (𝐴 × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wex 1781  wcel 2106  wne 2943  wral 3064  wrex 3073  Vcvv 3445  csb 3855  wss 3910  c0 4282  {csn 4586  cop 4592   ciun 4954   class class class wbr 5105   × cxp 5631  wf 6492  1-1wf1 6493  cfv 6496  (class class class)co 7357  1st c1st 7919  2nd c2nd 7920  m cmap 8765  cdom 8881  AC wacn 9874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-1st 7921  df-2nd 7922  df-map 8767  df-dom 8885  df-acn 9878
This theorem is referenced by:  iundomg  10477  iundom  10478
  Copyright terms: Public domain W3C validator